package tests;

import java.util.HashMap;
import java.util.Map;

import org.junit.After;
import org.junit.Before;
import org.junit.Test;

import substitution.HashUnifier;
import terms.Call;
import terms.Function;
import terms.AbstractTerm;
import terms.Variable;
import junit.framework.Assert;
import junit.framework.TestCase;

/**
 * 2 avr. 2012
 * @author Pierre Reliquet, Simon Devineau. Ecole des Mines de Nantes. Major in
 *         Information and Communications Systems Engineering.
 *         HashUnifierTest.java
 */
public class HashUnifierTest extends TestCase {
    /**
     * aDef a variable used to perform tests.
     */
    private Variable                        aDef;
    /**
     * cDef a variable used to perform tests.
     */
    private Variable                        cDef;
    /**
     * xDef a variable used to perform tests.
     */
    private Variable                        xDef;
    /**
     * yDef a variable used to perform tests.
     */
    private Variable                        yDef;
    /**
     * zDef a variable used to perform tests.
     */
    private Variable                        zDef;
    /**
     * fFuncDef a function used to perform tests.
     */
    private Function                        fFuncDef;
    /**
     * gFuncDef a function used to perform tests.
     */
    private Function                        gFuncDef;
    /**
     * kFuncDef a function used to perform tests.
     */
    private Function                        kFuncDef;
    /**
     * hFuncDef a function used to perform tests.
     */
    private Function                        hFuncDef;
    /**
     * fDeX a Call used to perform tests.
     */
    private Call                            fDeX;
    /**
     * fDeA a Call used to perform tests.
     */
    private Call                            fDeA;
    /**
     * gDeYA a Call used to perform tests.
     */
    private Call                            gDeYA;
    /**
     * hDeCZ a Call used to perform tests.
     */
    private Call                            hDeCZ;
    /**
     * kFirst a Call used to perform tests.
     */
    private Call                            kFirst;
    /**
     * fDeFDeA a Call used to perform tests.
     */
    private Call                            fDeFDeA;
    /**
     * fDeZ a Call used to perform tests.
     */
    private Call                            fDeZ;
    /**
     * gDeFDeZ a Call used to perform tests.
     */
    private Call                            gDeFDeZ;
    /**
     * fDeC a Call used to perform tests.
     */
    private Call                            fDeC;
    /**
     * hDeCEtFDeC a Call used to perform tests.
     */
    private Call                            hDeCEtFDeC;
    /**
     * kSecond a Call used to perform tests.
     */
    private Call                            kSecond;
    /**
     * hash a HashUnifier used to perform tests.
     */
    private HashUnifier                     hash;
    /**
     * result a Map of Terms which represents the results.
     */
    private Map<AbstractTerm, AbstractTerm> result;

    @Override
    @Before
    protected void setUp() throws Exception {
        aDef = new Variable("A");
        cDef = new Variable("C");
        xDef = new Variable("X");
        yDef = new Variable("Y");
        zDef = new Variable("Z");
        fFuncDef = new Function("f", Constants.ONE);
        gFuncDef = new Function("g", Constants.TWO);
        kFuncDef = new Function("k", Constants.THREE);
        hFuncDef = new Function("h", Constants.TWO);
        fDeX = new Call(fFuncDef);
        fDeX.addTerm(xDef);
        fDeA = new Call(fFuncDef);
        fDeA.addTerm(aDef);
        // /////////////
        // Premier K //
        // /////////////
        gDeYA = new Call(gFuncDef);
        gDeYA.addTerm(yDef);
        gDeYA.addTerm(aDef);
        hDeCZ = new Call(hFuncDef);
        hDeCZ.addTerm(cDef);
        hDeCZ.addTerm(zDef);
        kFirst = new Call(kFuncDef);
        kFirst.addTerm(fDeX);
        kFirst.addTerm(gDeYA);
        kFirst.addTerm(hDeCZ);
        // /////////////
        // Second K //
        // /////////////
        fDeFDeA = new Call(fFuncDef);
        fDeFDeA.addTerm(fDeA);
        fDeZ = new Call(fFuncDef);
        fDeZ.addTerm(zDef);
        gDeFDeZ = new Call(gFuncDef);
        gDeFDeZ.addTerm(fDeZ);
        gDeFDeZ.addTerm(aDef);
        fDeC = new Call(fFuncDef);
        fDeC.addTerm(cDef);
        hDeCEtFDeC = new Call(hFuncDef);
        hDeCEtFDeC.addTerm(cDef);
        hDeCEtFDeC.addTerm(fDeC);
        kSecond = new Call(kFuncDef);
        kSecond.addTerm(fDeFDeA);
        kSecond.addTerm(gDeFDeZ);
        kSecond.addTerm(hDeCEtFDeC);
        hash = new HashUnifier();
        hash.unify(kFirst, kSecond);
        hash.reduce();
        result = new HashMap<AbstractTerm, AbstractTerm>();
        final Call fResult = new Call(fFuncDef);
        final Call prov = new Call(fFuncDef);
        prov.addTerm(cDef);
        fResult.addTerm(prov);
        result.put(yDef, fResult);
        final Call fDeAResult = new Call(fFuncDef);
        fDeAResult.addTerm(aDef);
        result.put(xDef, fDeAResult);
        final Call fDeCResult = new Call(fFuncDef);
        fDeCResult.addTerm(cDef);
        result.put(zDef, fDeCResult);
    }

    @Override
    @After
    protected void tearDown() throws Exception {
        aDef = null;
        cDef = null;
        xDef = null;
        yDef = null;
        zDef = null;
        fFuncDef = null;
        gFuncDef = null;
        kFuncDef = null;
        hFuncDef = null;
        fDeX = null;
        fDeA = null;
        gDeYA = null;
        hDeCZ = null;
        kFirst = null;
        fDeFDeA = null;
        fDeZ = null;
        gDeFDeZ = null;
        fDeC = null;
        hDeCEtFDeC = null;
        kSecond = null;
        hash = null;
        result = null;
    }

    /**
     * Test method for
     * {@link substitution.HashUnifier#addToHashMap(terms.Variable, terms.AbstractTerm)}
     * .
     */
    @Test
    public void testAddToHashMap() {
        final int sizeBefore = hash.getMap().size();
        hash.addToHashMap(cDef, fDeX);
        final int sizeAfter = hash.getMap().size();
        Assert.assertTrue(sizeAfter == (sizeBefore + 1));
    }

    /**
     * Test method for
     * {@link substitution.HashUnifier#isVariable(java.lang.Object)}.
     */
    @Test
    public void testIsVariable() {
        Assert.assertTrue(HashUnifier.isVariable(aDef));
        Assert.assertFalse(HashUnifier.isVariable(fFuncDef));
    }

    /**
     * Test method for {@link substitution.HashUnifier#reduce()}.
     */
    @Test
    public void testReduce() {
        hash.unify(kFirst, kSecond);
        hash.reduce();
        Assert.assertTrue(result.equals(hash.getMap()));
        System.out.println("##############################################");
        System.out.println(hash.toString());
        System.out.println("##############################################");
    }

    /**
     * Test method for
     * {@link substitution.HashUnifier#substitute(terms.AbstractTerm, terms.AbstractTerm, terms.AbstractTerm)}
     * .
     */
    @Test
    public void testSubstitute() {
        final AbstractTerm t3 = HashUnifier.substitute(xDef, xDef, yDef);
        Assert.assertTrue(t3 instanceof Variable);
        final AbstractTerm t = HashUnifier.substitute(fDeC, cDef, xDef);
        Assert.assertTrue(t.equals(fDeX));
        final AbstractTerm t2 = HashUnifier.substitute(fDeFDeA, aDef, xDef);
        final Call verification = new Call(fFuncDef);
        verification.addTerm(fDeX);
        Assert.assertTrue(t2.equals(verification));
    }

    /**
     * Test method for {@link substitution.HashUnifier#toString()}.
     */
    @Test
    public void testToString() {
        hash.unify(kFirst, kSecond);
        hash.reduce();
        Assert.assertTrue(hash.toString().trim()
                .equals("{Y == f(f(C)) ; X == f(A) ; Z == f(C)}"));
    }

    /**
     * Test method for
     * {@link substitution.HashUnifier#unify(terms.AbstractTerm, terms.AbstractTerm)}
     * .
     */
    @Test
    public void testUnify() {
        hash.unify(fDeA, gDeYA);
        final int size = hash.getMap().size();
        assertTrue(size == 0);
        hash.unify(fDeA, fDeFDeA);
        final int size2 = hash.getMap().size();
        assertTrue(size2 == 0);
    }
}
